<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Table of contents</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/vfa.css" rel="stylesheet" type="text/css"/>

<script>

$(document).ready(function() {

    $("#accordion").show().accordion({
        autoHeight: false
    });

    $("#accordion div").css({ 'height': 'auto' });
});      


$( function() {
    var icons = {
      header: "ui-icon-circle-arrow-e",
      activeHeader: "ui-icon-circle-arrow-s"
    };
    
    $( "#accordion" ).accordion({
      icons: icons
    });
    $("#accordion").accordion({collapsible : true, active : 'none'});

    $( "#toggle" ).button().on( "click", function() {
      if ( $( "#accordion" ).accordion( "option", "icons" ) ) {
        $( "#accordion" ).accordion( "option", "icons", null );
      } else {
        $( "#accordion" ).accordion( "option", "icons", icons );
      }
    });
  } );
  </script>
<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 3: Verified Functional Algorithms</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</div>
</a></div>

<div id="main">

<div id="toc">
<div id="accordion">
<h2><a href="Preface.html">Preface</a></h2>
<div>
<ul class="doclist">
<li><a href="Preface.html">Top</a>
<li><a href="Preface.html#lab1">Welcome</a>

</li>
<li><a href="Preface.html#lab2">Practicalities</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab3">Chapter Dependencies</a>

</li>
<li><a href="Preface.html#lab4">System Requirements</a>

</li>
<li><a href="Preface.html#lab5">Exercises</a>

</li>
<li><a href="Preface.html#lab6">Downloading the Coq Files</a>

</li>
<li><a href="Preface.html#lab7">Lecture Videos</a>

</li>
<li><a href="Preface.html#lab8">For Instructors and Contributors</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab9">Thanks</a>

</li>
</ul>
</div>
<h2><a href="Perm.html">Basic Techniques for Permutations and Ordering&nbsp;&nbsp;&nbsp;&nbsp;(<i>Perm</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Perm.html">Top</a>
<li><a href="Perm.html#lab10">The Less-Than Order on the Natural Numbers</a>
<div>
<ul class="doclist">
<li><a href="Perm.html#lab11">Relating <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> to <span class="inlinecode"><span class="id" type="var">bool</span></span></a>

</li>
<li><a href="Perm.html#lab12">Some Advanced Tactical Hacking</a>

</li>
<li><a href="Perm.html#lab13"><span class="inlinecode"><span class="id" type="tactic">inversion</span></span> / <span class="inlinecode"><span class="id" type="tactic">clear</span></span> / <span class="inlinecode"><span class="id" type="tactic">subst</span></span></a>

</li>
<li><a href="Perm.html#lab14">Linear Integer Inequalities</a>

</li>
</ul>
</div>

</li>
<li><a href="Perm.html#lab15">Permutations</a>

</li>
<li><a href="Perm.html#lab19">Summary: Comparisons and Permutations</a>

</li>
</ul>
</div>
<h2><a href="Sort.html">Insertion Sort&nbsp;&nbsp;&nbsp;&nbsp;(<i>Sort</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Sort.html">Top</a>
<li><a href="Sort.html#lab21">Recommended Reading</a>

</li>
<li><a href="Sort.html#lab22">The Insertion-Sort Program</a>

</li>
<li><a href="Sort.html#lab23">Specification of Correctness</a>

</li>
<li><a href="Sort.html#lab24">Proof of Correctness</a>

</li>
<li><a href="Sort.html#lab29">Making Sure the Specification is Right</a>

</li>
<li><a href="Sort.html#lab32">Proving Correctness from the Alternate Spec</a>
<div>
<ul class="doclist">
<li><a href="Sort.html#lab36">The Moral of This Story</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Multiset.html">Insertion Sort With Multisets&nbsp;&nbsp;&nbsp;&nbsp;(<i>Multiset</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Multiset.html">Top</a>
<li><a href="Multiset.html#lab39">Correctness</a>

</li>
<li><a href="Multiset.html#lab43">Permutations and Multisets</a>

</li>
<li><a href="Multiset.html#lab50">The Main Theorem: Equivalence of Multisets and Permutations</a>

</li>
</ul>
</div>
<h2><a href="Selection.html">Selection Sort, With Specification and Proof of Correctness&nbsp;&nbsp;&nbsp;&nbsp;(<i>Selection</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Selection.html">Top</a>
<li><a href="Selection.html#lab51">The Selection-Sort Program</a>

</li>
<li><a href="Selection.html#lab52">Proof of Correctness of Selection sort</a>

</li>
<li><a href="Selection.html#lab57">Recursive Functions That are Not Structurally Recursive</a>

</li>
</ul>
</div>
<h2><a href="SearchTree.html">Binary Search Trees&nbsp;&nbsp;&nbsp;&nbsp;(<i>SearchTree</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="SearchTree.html">Top</a>
<li><a href="SearchTree.html#lab59">Total and Partial Maps</a>

</li>
<li><a href="SearchTree.html#lab60">Sections</a>

</li>
<li><a href="SearchTree.html#lab61">Program for Binary Search Trees</a>

</li>
<li><a href="SearchTree.html#lab62">Search Tree Examples</a>

</li>
<li><a href="SearchTree.html#lab63">What Should We Prove About Search trees?</a>

</li>
<li><a href="SearchTree.html#lab64">Efficiency of Search Trees</a>

</li>
<li><a href="SearchTree.html#lab65">Proof of Correctness</a>

</li>
<li><a href="SearchTree.html#lab70">Correctness Proof of the <span class="inlinecode"><span class="id" type="var">elements</span></span> Function</a>

</li>
<li><a href="SearchTree.html#lab73">Representation Invariants</a>
<div>
<ul class="doclist">
<li><a href="SearchTree.html#lab76">Auxiliary Lemmas About <span class="inlinecode"><span class="id" type="var">In</span></span> and <span class="inlinecode"><span class="id" type="var">list2map</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="SearchTree.html#lab78">Preservation of Representation Invariant</a>

</li>
<li><a href="SearchTree.html#lab81">We Got Lucky</a>

</li>
<li><a href="SearchTree.html#lab82">Every Well-Formed Tree Does Actually Relate to an Abstraction</a>

</li>
<li><a href="SearchTree.html#lab85">It Wasn't Really Luck, Actually</a>
<div>
<ul class="doclist">
<li><a href="SearchTree.html#lab87">Coherence With <span class="inlinecode"><span class="id" type="var">elements</span></span> Instead of <span class="inlinecode"><span class="id" type="var">lookup</span></span></a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="ADT.html">Abstract Data Types&nbsp;&nbsp;&nbsp;&nbsp;(<i>ADT</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ADT.html">Top</a>
<li><a href="ADT.html#lab89">A Brief Excursion into Dependent Types</a>

</li>
<li><a href="ADT.html#lab91">Summary of Abstract Data Type Proofs</a>

</li>
<li><a href="ADT.html#lab92">Exercise in Data Abstraction</a>

</li>
</ul>
</div>
<h2><a href="Extract.html">Running Coq programs in ML&nbsp;&nbsp;&nbsp;&nbsp;(<i>Extract</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Extract.html">Top</a>
<li><a href="Extract.html#lab95">Utilities for OCaml Integer Comparisons</a>

</li>
<li><a href="Extract.html#lab96">SearchTrees, Extracted</a>
<div>
<ul class="doclist">
<li><a href="Extract.html#lab97">Maps, on <span class="inlinecode"><span class="id" type="var">Z</span></span> Instead of <span class="inlinecode"><span class="id" type="var">nat</span></span></a>

</li>
<li><a href="Extract.html#lab98">Trees, on <span class="inlinecode"><span class="id" type="var">int</span></span> Instead of <span class="inlinecode"><span class="id" type="var">nat</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="Extract.html#lab102">Performance Tests</a>

</li>
<li><a href="Extract.html#lab103">Unbalanced Binary Search Trees</a>

</li>
<li><a href="Extract.html#lab104">Balanced Binary Search Trees</a>

</li>
</ul>
</div>
<h2><a href="Redblack.html">Implementation and Proof of Red-Black Trees&nbsp;&nbsp;&nbsp;&nbsp;(<i>Redblack</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Redblack.html">Top</a>
<li><a href="Redblack.html#lab105">Required Reading</a>

</li>
<li><a href="Redblack.html#lab106">Proof Automation for Case-Analysis Proofs.</a>

</li>
<li><a href="Redblack.html#lab107">The SearchTree Property</a>

</li>
<li><a href="Redblack.html#lab114">Proving Efficiency</a>

</li>
<li><a href="Redblack.html#lab116">Extracting and Measuring Red-Black Trees</a>

</li>
<li><a href="Redblack.html#lab117">Success!</a>

</li>
</ul>
</div>
<h2><a href="Trie.html">Number Representations and Efficient Lookup Tables&nbsp;&nbsp;&nbsp;&nbsp;(<i>Trie</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Trie.html">Top</a>
<li><a href="Trie.html#lab118">LogN Penalties in Functional Programming</a>

</li>
<li><a href="Trie.html#lab119">A Simple Program That's Waaaaay Too Slow.</a>

</li>
<li><a href="Trie.html#lab120">Efficient Positive Numbers</a>
<div>
<ul class="doclist">
<li><a href="Trie.html#lab124">Coq's Integer Type, <span class="inlinecode"><span class="id" type="var">Z</span></span></a>

</li>
<li><a href="Trie.html#lab125">From <span class="inlinecode"><span class="id" type="var">N</span>*<span class="id" type="var">N</span>*<span class="id" type="var">N</span></span> to <span class="inlinecode"><span class="id" type="var">N</span>*<span class="id" type="var">N</span>*<span class="id" type="var">logN</span></span></a>

</li>
<li><a href="Trie.html#lab126">From <span class="inlinecode"><span class="id" type="var">N</span>*<span class="id" type="var">N</span>*<span class="id" type="var">logN</span></span> to <span class="inlinecode"><span class="id" type="var">N</span>*<span class="id" type="var">logN</span>*<span class="id" type="var">logN</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="Trie.html#lab127">Tries: Efficient Lookup Tables on Positive Binary Numbers</a>
<div>
<ul class="doclist">
<li><a href="Trie.html#lab128">From <span class="inlinecode"><span class="id" type="var">N</span>*<span class="id" type="var">logN</span>*<span class="id" type="var">logN</span></span> to <span class="inlinecode"><span class="id" type="var">N</span>*<span class="id" type="var">logN</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="Trie.html#lab130">Proving the Correctness of Trie Tables</a>
<div>
<ul class="doclist">
<li><a href="Trie.html#lab131">Lemmas About the Relation Between <span class="inlinecode"><span class="id" type="var">lookup</span></span> and <span class="inlinecode"><span class="id" type="var">insert</span></span></a>

</li>
<li><a href="Trie.html#lab135">Bijection Between <span class="inlinecode"><span class="id" type="var">positive</span></span> and <span class="inlinecode"><span class="id" type="var">nat</span></span>.</a>

</li>
<li><a href="Trie.html#lab137">Proving That Tries are a "Table" ADT.</a>

</li>
<li><a href="Trie.html#lab142">Sanity Check</a>

</li>
</ul>
</div>

</li>
<li><a href="Trie.html#lab143">Conclusion</a>

</li>
</ul>
</div>
<h2><a href="Priqueue.html">Priority Queues&nbsp;&nbsp;&nbsp;&nbsp;(<i>Priqueue</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Priqueue.html">Top</a>
<li><a href="Priqueue.html#lab144">Module Signature</a>

</li>
<li><a href="Priqueue.html#lab145">Implementation</a>
<div>
<ul class="doclist">
<li><a href="Priqueue.html#lab146">Some Preliminaries</a>

</li>
<li><a href="Priqueue.html#lab148">The Program</a>

</li>
</ul>
</div>

</li>
<li><a href="Priqueue.html#lab149">Predicates on Priority Queues</a>
<div>
<ul class="doclist">
<li><a href="Priqueue.html#lab150">The Representation Invariant</a>

</li>
<li><a href="Priqueue.html#lab151">Sanity Checks on the Abstraction Relation</a>

</li>
<li><a href="Priqueue.html#lab152">Characterizations of the Operations on Queues</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Binom.html">Binomial Queues&nbsp;&nbsp;&nbsp;&nbsp;(<i>Binom</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Binom.html">Top</a>
<li><a href="Binom.html#lab154">Required Reading</a>

</li>
<li><a href="Binom.html#lab155">The Program</a>

</li>
<li><a href="Binom.html#lab156">Characterization Predicates</a>

</li>
<li><a href="Binom.html#lab157">Proof of Algorithm Correctness</a>
<div>
<ul class="doclist">
<li><a href="Binom.html#lab158">Various Functions Preserve the Representation Invariant</a>

</li>
<li><a href="Binom.html#lab165">The Abstraction Relation</a>

</li>
<li><a href="Binom.html#lab167">Sanity Checks on the Abstraction Relation</a>

</li>
<li><a href="Binom.html#lab173">Various Functions Preserve the Abstraction Relation</a>

</li>
<li><a href="Binom.html#lab176">Optional Exercises</a>

</li>
</ul>
</div>

</li>
<li><a href="Binom.html#lab183">Measurement.</a>

</li>
</ul>
</div>
<h2><a href="Decide.html">Programming with Decision Procedures&nbsp;&nbsp;&nbsp;&nbsp;(<i>Decide</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Decide.html">Top</a>
<li><a href="Decide.html#lab185">Using <span class="inlinecode"><span class="id" type="var">reflect</span></span> to characterize decision procedures</a>

</li>
<li><a href="Decide.html#lab186">Using <span class="inlinecode"><span class="id" type="var">sumbool</span></span> to Characterize Decision Procedures</a>
<div>
<ul class="doclist">
<li><a href="Decide.html#lab187"><span class="inlinecode"><span class="id" type="var">sumbool</span></span> in the Coq Standard Library</a>

</li>
</ul>
</div>

</li>
<li><a href="Decide.html#lab189">Decidability and Computability</a>

</li>
<li><a href="Decide.html#lab190">Opacity of <span class="inlinecode"><span class="id" type="keyword">Qed</span></span></a>

</li>
<li><a href="Decide.html#lab192">Advantages and Disadvantages of <span class="inlinecode"><span class="id" type="var">reflect</span></span> Versus <span class="inlinecode"><span class="id" type="var">sumbool</span></span></a>

</li>
</ul>
</div>
<h2><a href="Color.html">Graph Coloring&nbsp;&nbsp;&nbsp;&nbsp;(<i>Color</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Color.html">Top</a>
<li><a href="Color.html#lab193">Preliminaries: Representing Graphs</a>

</li>
<li><a href="Color.html#lab194">Lemmas About Sets and Maps</a>
<div>
<ul class="doclist">
<li><a href="Color.html#lab195">equivlistA</a>

</li>
<li><a href="Color.html#lab196">SortA_equivlistA_eqlistA</a>

</li>
<li><a href="Color.html#lab197">S.remove and S.elements</a>

</li>
<li><a href="Color.html#lab199">Lists of (key,value) Pairs</a>

</li>
<li><a href="Color.html#lab202">Cardinality</a>

</li>
</ul>
</div>

</li>
<li><a href="Color.html#lab209">Now Begins the Graph Coloring Program</a>
<div>
<ul class="doclist">
<li><a href="Color.html#lab210">Some Proofs in Support of Termination</a>

</li>
<li><a href="Color.html#lab213">The Rest of the Algorithm</a>

</li>
</ul>
</div>

</li>
<li><a href="Color.html#lab214">Proof of Correctness of the Algorithm.</a>

</li>
<li><a href="Color.html#lab218">Trying Out the Algorithm on an Actual Test Case</a>

</li>
</ul>
</div>
</div>
</div>

</div>

</div>
</body>
</html>